Nuprl Lemma : ecl-trans-state-from-append 0,22
ds:x:Id fp Type, da:k:Knd fp Type, v:ecl-trans-tuple{i:l}(ds;da), z:Top, L1, L2:Top List.
ecl-trans-state-from(v;z;L1 @ L2) ~ ecl-trans-state-from(v;ecl-trans-state-from(v;z;L1);L2) 
latex

Definitionslet a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), ecl-trans-tuple{i:l}(ds;da), t  T, Top, x,y. t(x;y), x:A. B(x), ecl-trans-state-from(v;z;L), Id, x. t(x), a:A fp B(a), Knd
Lemmastop wf, ecl-trans-tuple wf, Knd wf, fpf wf, Id wf, list accum append

origin